Computationally sound implementations of equational theories against passive adversaries
Identifieur interne : 003B86 ( Main/Exploration ); précédent : 003B85; suivant : 003B87Computationally sound implementations of equational theories against passive adversaries
Auteurs : Mathieu Baudet [France] ; Véronique Cortier [France] ; Steve Kremer [France]Source :
- Information and computation : (Print) [ 0890-5401 ] ; 2009.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
In this paper we study the link between formal and cryptographic models for security protocols in the presence of passive adversaries. In contrast to other works, we do not consider a fixed set of primitives but aim at results for arbitrary equational theories. We define a framework for comparing a cryptographic implementation and its idealization with respect to various security notions. In particular, we concentrate on the computational soundness of static equivalence, a standard tool in cryptographic pi calculi. We present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, to illustrate our framework, we establish the soundness of static equivalence for the exclusive OR and a theory of ciphers and lists.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000276
- to stream PascalFrancis, to step Curation: 000751
- to stream PascalFrancis, to step Checkpoint: 000251
- to stream Main, to step Merge: 003C85
- to stream Hal, to step Corpus: 001747
- to stream Hal, to step Curation: 001747
- to stream Hal, to step Checkpoint: 002F80
- to stream Main, to step Merge: 003858
- to stream Main, to step Curation: 003B86
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Computationally sound implementations of equational theories against passive adversaries</title><author><name sortKey="Baudet, Mathieu" sort="Baudet, Mathieu" uniqKey="Baudet M" first="Mathieu" last="Baudet">Mathieu Baudet</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>DCSSI</s1><s2>Paris</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Île-de-France</region><region type="old region">Île-de-France</region><settlement type="city">Paris</settlement></placeName></affiliation></author><author><name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Loria/CNRS &/INRIA Lorraine Projet Cassis</s1><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>Loria/CNRS &/INRIA Lorraine Projet Cassis</wicri:noRegion><wicri:noRegion>Loria/CNRS &/INRIA Lorraine Projet Cassis</wicri:noRegion></affiliation></author><author><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name><affiliation wicri:level="1"><inist:fA14 i1="03"><s1>LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan</s1><s3>FRA</s3><sZ>3 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan</wicri:noRegion><wicri:noRegion>LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">09-0176595</idno><date when="2009">2009</date><idno type="stanalyst">PASCAL 09-0176595 INIST</idno><idno type="RBID">Pascal:09-0176595</idno><idno type="wicri:Area/PascalFrancis/Corpus">000276</idno><idno type="wicri:Area/PascalFrancis/Curation">000751</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000251</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000251</idno><idno type="wicri:doubleKey">0890-5401:2009:Baudet M:computationally:sound:implementations</idno><idno type="wicri:Area/Main/Merge">003C85</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00426620</idno><idno type="url">https://hal.inria.fr/inria-00426620</idno><idno type="wicri:Area/Hal/Corpus">001747</idno><idno type="wicri:Area/Hal/Curation">001747</idno><idno type="wicri:Area/Hal/Checkpoint">002F80</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">002F80</idno><idno type="wicri:doubleKey">0890-5401:2009:Baudet M:computationally:sound:implementations</idno><idno type="wicri:Area/Main/Merge">003858</idno><idno type="wicri:Area/Main/Curation">003B86</idno><idno type="wicri:Area/Main/Exploration">003B86</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Computationally sound implementations of equational theories against passive adversaries</title><author><name sortKey="Baudet, Mathieu" sort="Baudet, Mathieu" uniqKey="Baudet M" first="Mathieu" last="Baudet">Mathieu Baudet</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>DCSSI</s1><s2>Paris</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Île-de-France</region><region type="old region">Île-de-France</region><settlement type="city">Paris</settlement></placeName></affiliation></author><author><name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Loria/CNRS &/INRIA Lorraine Projet Cassis</s1><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>Loria/CNRS &/INRIA Lorraine Projet Cassis</wicri:noRegion><wicri:noRegion>Loria/CNRS &/INRIA Lorraine Projet Cassis</wicri:noRegion></affiliation></author><author><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name><affiliation wicri:level="1"><inist:fA14 i1="03"><s1>LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan</s1><s3>FRA</s3><sZ>3 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan</wicri:noRegion><wicri:noRegion>LSV/CNRS & INRIA Saclay Projet SECSI & ENS Cachan</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Information and computation : (Print)</title><title level="j" type="abbreviated">Inf. comput. : (Print)</title><idno type="ISSN">0890-5401</idno><imprint><date when="2009">2009</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Information and computation : (Print)</title><title level="j" type="abbreviated">Inf. comput. : (Print)</title><idno type="ISSN">0890-5401</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computer theory</term><term>Equational theory</term><term>Equivalence</term><term>Implementation</term><term>Link</term><term>Primitive</term><term>Security protocol</term><term>Soundness</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Implémentation</term><term>Théorie équationnelle</term><term>Lien</term><term>Primitif</term><term>Consistance sémantique</term><term>Equivalence</term><term>Informatique théorique</term><term>Protocole sécurité</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">In this paper we study the link between formal and cryptographic models for security protocols in the presence of passive adversaries. In contrast to other works, we do not consider a fixed set of primitives but aim at results for arbitrary equational theories. We define a framework for comparing a cryptographic implementation and its idealization with respect to various security notions. In particular, we concentrate on the computational soundness of static equivalence, a standard tool in cryptographic pi calculi. We present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, to illustrate our framework, we establish the soundness of static equivalence for the exclusive OR and a theory of ciphers and lists.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Île-de-France</li></region><settlement><li>Paris</li></settlement></list><tree><country name="France"><region name="Île-de-France"><name sortKey="Baudet, Mathieu" sort="Baudet, Mathieu" uniqKey="Baudet M" first="Mathieu" last="Baudet">Mathieu Baudet</name></region><name sortKey="Cortier, Veronique" sort="Cortier, Veronique" uniqKey="Cortier V" first="Véronique" last="Cortier">Véronique Cortier</name><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003B86 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003B86 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:09-0176595
|texte= Computationally sound implementations of equational theories against passive adversaries
}}
| This area was generated with Dilib version V0.6.33. |  |